1. Field of the Invention
This invention relates to computer aided design verification. More particularly, this invention relates to graphical techniques for explicitly assigning behaviors to hardware design inputs.
2. Description of the Related Art
TABLE 1Acronyms and AbbreviationsDFTDesign-For-TestDUTDesign-Under-TestFVFormal VerificationHDLHardware Description LanguagePSLProperty Specification LanguageRAMRandom Access MemoryRTLRegister Transfer LevelVHDLVHSIC Hardware Description LanguageVHSICVery High Speed Integrated CircuitsXMLeXtensible Markup Language
Formal verification (FV) has gained momentum in recent years and is now an important step in the process of validating a hardware design. For example, formal verification can pinpoint corner-case misbehaviors in a search space. However, due to the potential of formal verification to search a state space exhaustively, formal verification engineers must be careful to ensure that the verification of the design-under-test (DUT) deals only with legal inputs. In other words, design input behavior must reflect an agreed protocol between a design-under-test and its surrounding hardware modules. This agreed protocol is usually referred to as the environment of the design-under-test.
Design inputs can be assigned legal behavior in two ways: in one approach, a hardware description language (HDL), such as Verilog®, specifies either a combinational function or a next-state function for each design input. Formal verification tools usually require that only synthesizable constructs are to be used for that purpose. Most behavioral constructs are not allowed.
In a second approach a declarative language, such as Process Specification Language (PSL), described in ISO 18629 of the International Standards Organization, is used to specify temporal conditions on the behavior of a design input, e.g., “The input ack will always be asserted two cycles after the output req was asserted”.
In either case, specifying the environment manually, even with the aid of one of the above-described alternatives, remains one of the most labor-intensive tasks in a formal verification project. Every design input must be assigned an appropriate and correct behavior. The assignment should not be too restrictive, lest design flaws may escape detection. Neither should it be too loose, in order to prevent the false detection of spurious design flaws. It is indeed a tedious and repetitive task.